Formale Semantik

Dieser Text beschreibt Formale Semantik.

Die formale Semantik ist ein Teilgebiet der theoretischen Informatik, das sich mit dem Nachweis der Korrektheit von Computerprogrammen beschäftigt (Verifikation). Anders als die Semantik, die ein Teil der Sprachwissenschaft ist, arbeitet die formale Semantik mit vollständig mathematischen Methoden, um die Bedeutung von Computerprogrammen und Spezifikationen zu formalisieren. Sie ist eng verwandt mit der Berechenbarkeitstheorie, die sich damit beschäftigt, welche Probleme mit Computerprogrammen überhaupt gelöst werden können.

Die formale Semantik gliedert sich in

• denotationale Semantik: Konstruktion der Semantik mittels mathematischer Räume aus der domain theory , die Semantik eines Programms ist eine Funktion
• axiomatische Semantik : Beschreibung der Semantik durch ihre logischen Merkmale, wobei i.a. ca. einiges Merkmalen betrachtet werden
• operationale Semantik: durch eine Relation werden die möglichen Ausführungsschritte als Paare (Programm, Zustand) beschrieben.